STRATEGIE AGENTI: [{'condition_action_pairs': [('a', 'A'), ('!a', 'B')]}, {'condition_action_pairs': [('a', 'C'), ('!a', 'D')]}, {'condition_action_pairs': [('a', 'Y'), ('!a', 'Z')]}]
[['III', 'ACZ,ADY', 'BCZ,BDY', 'ICZ'], [0, 'III', 'ADZ,BDZ', 'ACZ,BCY'], ['ACY,BDZ', 'ICZ', 'III', 'ADZ,BCY'], [0, 'AIZ', 0, 'III']]
[['s0', 's0', 's0', 's0'], [None, 's1', 's1', 's1'], ['s2', 's2', 's2', 's2'], [None, 's3', None, 's3']]
agent_key:actions_agent1
['A', 'B']
agent_key:actions_agent2
['C', 'D']
agent_key:actions_agent3
['Y', 'Z']
condizione a
a
risultato m_checking{'res': "Result: {'s3', 's0'}", 'initial_state': 'Initial state s0: True'}, statesRES Result: {'s3', 's0'}
state_set: {'s3', 's0'} con iteration 0 action A
states:{'s3', 's0'}
Prima iterazione modify per agente 1
new transition matrix: [['III', 'ACZ,ADY', 0, 'ICZ'], [0, 'III', 'ADZ,BDZ', 'ACZ,BCY'], ['ACY,BDZ', 'ICZ', 'III', 'ADZ,BCY'], [0, 'AIZ', 0, 'III']]
condizione !a
('!', 'a')
risultato m_checking{'res': "Result: {'s1', 's2'}", 'initial_state': 'Initial state s0: False'}, statesRES Result: {'s1', 's2'}
state_set: {'s1', 's2'} con iteration 1 action B
states:{'s1', 's2'}
seconda iterazione modify per agente 1
new transition matrix: [['III', 'ACZ,ADY', 0, 'ICZ'], [0, 'III', 'BDZ', 'BCY'], ['BDZ', 'ICZ', 'III', 'BCY'], [0, 'AIZ', 0, 'III']]
condizione a
a
risultato m_checking{'res': "Result: {'s3', 's0'}", 'initial_state': 'Initial state s0: True'}, statesRES Result: {'s3', 's0'}
state_set: {'s3', 's0'} con iteration 0 action C
states:{'s3', 's0'}
Prima iterazione modify per agente 2
new transition matrix: [['III', 'ACZ', 0, 'ICZ'], [0, 'III', 'BDZ', 'BCY'], ['BDZ', 'ICZ', 'III', 'BCY'], [0, 'AIZ', 0, 'III']]
condizione !a
('!', 'a')
risultato m_checking{'res': "Result: {'s1', 's2'}", 'initial_state': 'Initial state s0: False'}, statesRES Result: {'s1', 's2'}
state_set: {'s1', 's2'} con iteration 1 action D
states:{'s1', 's2'}
seconda iterazione modify per agente 2
new transition matrix: [['III', 'ACZ', 0, 'ICZ'], [0, 'III', 'BDZ', 0], ['BDZ', 0, 'III', 0], [0, 'AIZ', 0, 'III']]
condizione a
a
risultato m_checking{'res': "Result: {'s3', 's0'}", 'initial_state': 'Initial state s0: True'}, statesRES Result: {'s3', 's0'}
state_set: {'s3', 's0'} con iteration 0 action Y
states:{'s3', 's0'}
Prima iterazione modify per agente 3
new transition matrix: [['III', 0, 0, 0], [0, 'III', 'BDZ', 0], ['BDZ', 0, 'III', 0], [0, 0, 0, 'III']]
condizione !a
('!', 'a')
risultato m_checking{'res': "Result: {'s1', 's2'}", 'initial_state': 'Initial state s0: False'}, statesRES Result: {'s1', 's2'}
state_set: {'s1', 's2'} con iteration 1 action Z
states:{'s1', 's2'}
seconda iterazione modify per agente 3
new transition matrix: [['III', 0, 0, 0], [0, 'III', 'BDZ', 0], ['BDZ', 0, 'III', 0], [0, 0, 0, 'III']]
('AX', 'h')
sono dentro
states stringati da node left (in cui è verificato l'atomo complementato: set()
transizioni passate in input: [('s0', 's0'), ('s1', 's1'), ('s1', 's2'), ('s2', 's0'), ('s2', 's2'), ('s3', 's3')]
sto facendo pre, questi sono gli stati in cui la proposizione atomica è valida: set()
{'res': "Result: {'s3', 's0', 's1', 's2'}", 'initial_state': 'Initial state s0: True'}
Solution: {'res': "Result: {'s3', 's0', 's1', 's2'}", 'initial_state': 'Initial state s0: True'}
flag: True
Solution found!

